\chapter{Preliminares} 
Con el objetivo de presentar los fundamentos utilizados en este trabajo, en este capítulo se brindará una introducción a la \textit{Lógica Modal} y posteriormente dos lógicas modales particulares, la Lógica Temporal de Tiempo Lineal (\emph{LTL}) y una extensión de la misma con el concepto de "Fluente". Está última, denominada Lógica Temporal de Tiempo Lineal con Fluentes (\emph{FLTL}) nos va permitir expresar las propiedades antes mencionadas. Luego se presentarán algunos de los lenguajes destacados para la descripción de Procesos de Negocios, entre ellos \emph{YAWL}, el cual será el lenguaje elegido para el análisis automático de propiedades. Finalmente introduciremos fundamentos formales para poder llevar a cabo la verificación: Sistemas de Transición de Estados y un Álgebra de Procesos que permite especificarlos de manera compacta.

\section{Lógica Modal}
La lógica modal es una extensión de la lógica proposicional que permite el uso de operadores que expresan modalidades. Considérese el siguiente ejemplo, en donde se toma una simple afirmación en lógica proposicional, tal como lo es:
$$ p  = \textit{``llueve''}$$
Si, en cambio de afirmar que en el instante dado llueve, se deseara expresar que en un futuro lloverá, se necesitará una variable proposicional totalmente distinta. Esto podrá conseguirse de la siguiente manera:
$$ q  = \textit{``finalmente lloverá''}$$
Sin embargo, si se quisiera explotar el hecho de que las formulas tiene algo en común -una asevera del el futuro lo que la otra del presente-, se encontraría que no existe un modo directo de conseguir tal cosa.
Sin embargo, en lógica modal, es posible utilizar modalidades de modo tal que la variable proposicional p sea la misma en ambas sentencias, y la segunda se obtenga a partir de la primera mediante el uso de un operador modal:
$$ p  = \textit{``llueve''}$$
$$q  = \Diamond{p}$$
en donde el operador modal \text{$\Diamond$} es interpretado como ``finalmente''.
\subsection{Definición Formal}
En esta sección se introduce la definición formal de lógica modal. Cabe aclarar que la definición de la semántica de éstas puede variar según la fuente consultada. La aproximación expuesta aquí es quizás la más común e intuitiva.
A continuación se define la sintaxis de una lógica modal, así como su semántica. Ésta última está basada en un modelo relacional. De este modo la lógica modal puede ser pensada como una lógica que permite hablar de estructuras, mas precisamente, grafos.
\paragraph{}
\noindent \textbf{Sintaxis}\\
Supongamos que se cuenta con dos conjuntos:  \textit{PROP}, un conjunto de variables proposicionales, y  \textit{MOD}, un conjunto de modalidades u operadores modales. La elección de \textit{PROP} y \textit{MOD} define la signatura de una lógica modal. Asumiremos que \textit{PROP} en un conjunto
infinito enumerable. Las fórmulas sobre la signatura $\la PROP,MOD\ra$  se definen como sigue:
$$\varphi := p | true | false | \neg\varphi | \varphi \wedge \psi | \varphi \vee \psi | \square^m \varphi | \Diamond^m \varphi$$
en donde $p \in PROP; m \in MOD$. Esto significa que una fórmula modal es una proposición, una composición de fórmulas en base a los operadores usuales (conjunción, disyunción, negación), o la introducción de un operador modal sobre una fórmula. Existe cierta redundancia en esta definición ya que, como en la lógica proposicional, sólo hace falta la negación y un operador binario para definir el resto. De manera similar, las modalidades $\Diamond$ y $\Box$  son duales del mismo modo que los cuantificadores de primer order. Es decir, $\Box^m\varphi = \neg\Diamond^m\neg\varphi$.\\
En el caso de que el conjunto de modalidades sea unitario simplemente se escribe $\Box$ y $\Diamond$, en
lugar de $\Box^m$  y $\Diamond^m$.
\paragraph{}
\noindent \textbf{Semántica}\\
Un modelo (usualmente llamados modelos de Kripke\cite{Schneider2004}) de un lenguaje modal es una estructura $\mathfrak{M} = (W, \{R\}_{m\in MOD}, V )$. El conjunto $W$ es el dominio de la estructura (también se suele referir a $W$ como conjunto de lugares, mundos, estados, etc.). El conjunto $\{R\}_{m\in MOD}$ es un conjunto de relaciones binarias entre los elementos de $W$, y $V$ es una función de valoración que asigna a cada $p \in PROP$ un conjunto de puntos de $\mathfrak{M}$ en donde $p$ es verdadera. En el caso de que haya sólo una modalidad, la estructura se escribirá simplemente como $\mathfrak{M} = (W,R, V )$. Es necesario remarcar que este tipo de estructuras puede pensarse como una colección de grafos dirigidos, uno por cada relación $R_m$.
Dado un modelo $\mathfrak{M} = (W, \{R\}_{m\in MOD}, V )$ y un punto $w$ del modelo, la noción de satisfactibilidad (es decir, de que una fórmula sea verdadera en un punto dado del modelo) se define como sigue:

\small{
\begin{equation*}
\begin{aligned}[t]
&\mathfrak{M}, w \models p\\
&\mathfrak{M}, w \models \textbf{true}\\
&\mathfrak{M}, w \models \textbf{false}\\
&\mathfrak{M}, w \models \neg\varphi\\
&\mathfrak{M}, w \models \varphi \wedge\psi\\
&\mathfrak{M}, w \models \varphi \vee \psi\\
&\mathfrak{M}, w \models \Box^m\varphi\\
&\mathfrak{M}, w \models \Diamond^m\varphi
\end{aligned}
\qquad
\begin{aligned}[t]
&\textbf{sii}\\
&\:\\
&\:\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
\end{aligned}
\qquad
\begin{aligned}[t]
&w\in V(p)\\
&siempre\\
&nunca\\
&no\: \mathfrak{M}, w  \models  \varphi\\
&\mathfrak{M}, w \models \varphi \text{ y } \mathfrak{M}, w \models \psi\\
&\mathfrak{M}, w \models \varphi \text{ ó } \mathfrak{M}, w \models \psi\\
&\text{para todo } v \in W \text{ tal que } R^m wv \text{ se tiene que } \mathfrak{M}, v \models \varphi\\
&\text{para algún } v \in W \text{ tal que } R^m wv \text{ se tiene que } \mathfrak{M}, v \models \varphi\\
\end{aligned}
\end{equation*}}

Esta definición de semántica es análoga a la de lógica proposicional, con diferencias en cuanto a la interpretación de las variables proposicionales (y desde luego con respecto a los operadores modales). En lógica modal (al menos con la semántica aquí presentada), una variable proposicional no es verdadera o falsa por si, sino que su valor de verdad depende del punto del modelo donde se la evalúe. De este modo puede darse el caso que una variable proposicional sea falsa en algunos puntos del modelo y verdadera en otros (es fácil corroborar en la definición que no pueden darse ambas). Dado que el valor de verdad de las variables proposicionales depende del punto del modelo en que se evalúen (y de que la semántica para los operadores $\neg$,$\wedge$,$\vee$ es la usual), es necesario encontrar algún modo de poder relacionar los valores de verdad de las proposiciones en los diferentes puntos del modelo. Esta función recae sobre los operadores $\Box$ y $\Diamond$ . Su función puede explicarse como sigue:

\begin{itemize}
\item \textbf{Operador} $\Diamond$ : Una fórmula del tipo $\Diamond^m\psi$  vale en un punto el modelo si y solo si $\psi$ vale en algún sucesor del punto actual vía la relación de transición $R^m$. Podría entenderse como sigue:
$$\Diamond^m\psi =  \textit{``En algún m-sucesor (de este punto) vale'' } \psi $$
\item \textbf{Operador} $\Box$ : Una fórmula del tipo $\Box^m\psi$  vale en un punto el modelo si y solo si vale en todos los sucesores del punto actual vía la relación de transición $R^m$. Podría entenderse como sigue:
$$\Box^m\psi =  \textit{``En todo m-sucesor (de este punto) vale'' } \psi $$
\end{itemize}

\section{Lógica Temporal de Tiempo Lineal}
Tradicionalmente, en la práctica de diseñar algoritmos, es deseable corroborar que éstos terminan y, más aún, que lo hacen en un estado correcto. A este fin normalmente se utiliza algún tipo de cálculo como, por ejemplo, la lógica de Hoare. Sin embargo, existe otro tipo de sistemas que no responde a esta clasificación: aquellos que en vez de llevar a cabo una computación y terminar, continúan su ejecución infinitamente reaccionando a eventos externos. Algunos ejemplos de tales sistemas son: programas en servidores (web servers, servidores de correo, servidores FTP), máquinas expendedoras, entre otros. A este tipo de sistemas se los denomina \textit{sistemas reactivos}.
Está claro que sería incorrecto describir un programa del tipo de un servidor web como un proceso con terminación: se ejecuta la aplicación, luego de responder a una petición ésta termina, para atender más pedidos se la debe volver a iniciar. A estos sistemas se les puede verificar las siguientes dos propiedades.
\linebreak 

\begin{itemize}
\item\textit{Safety}: Aseguran que el sistema no puede alcanzar un determinado estado (indeseable).
Usualmente toman la siguiente forma:
$$\textit{``Nunca ocurre que } \varphi \textit{''}$$

En donde $ \varphi $  caracteriza en hecho de que el sistema se encuentre en el estado indeseable. Un ejemplo de estas propiedades es la ausencia de \textit{deadlock}.


\item\textit{Liveness}: Aseguran que cierta propiedad (deseable) siempre valdría en el futuro. Usualmente
toman la siguiente forma:
$$\textit{``Siempre ocurre que, finalmente ocurre } \varphi \textit{''}$$


En donde $ \varphi $ caracteriza una cierta propiedad deseable en el sistema. Un ejemplo de este tipo de propiedades son aquellas que garantizan que el sistema siempre producirá una respuesta ante un evento dado.
\end{itemize}

\subsection{Sintaxis}
Supongase que se cuneta con un conjunto de nombres de variables proposicionales \textit{PROP} entonces, las fórmulas \emph{LTL} están definidas inductivamente como sigue:
$$\varphi := p | true | false | \neg\varphi | \varphi \wedge \psi | \varphi \vee \psi | X \varphi | \varphi U \psi$$

Según esto, toda variable proposicional es una fórmula. La negación, disyunción y conjunción de fórmulas también lo es. Por último en \emph{LTL} hay dos operadores temporales: next(X) y until (U). A partir de éstos se definen los operadores temporales F (eventually), G(always) y W (weak until ): $ F \psi \equiv true U \psi, G\psi \equiv \neg F \neg\psi, and \psi W   \equiv ((\psi U \varphi ) \vee G \psi)$.

\subsection{Semántica}
Los modelos sobre los cuales se interpretan las fórmulas de lógica temporal son secuencias infinitas $w = x_0x_1x_2 ...$ en donde $x_i$ $\in$ $\wp$(PROP). Intuitivamente es una secuencia infinita en donde para cada punto se indica cuales son las variables proposicionales que son verdaderas. La noción de satisfactibilidad se define como sigue:

\small{
\begin{equation*}
\begin{aligned}[t]
& w \models p\\
& w \models \textbf{true}\\
& w \models \textbf{false}\\
& w \models \neg\varphi\\
& w \models \varphi \wedge\psi\\
& w \models \varphi \vee \psi\\
& w \models X\varphi\\
& w \models \psi U \varphi
\end{aligned}
\qquad
\begin{aligned}[t]
&\textbf{sii}\\
&\:\\
&\:\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
&\textbf{sii}\\
\end{aligned}
\qquad
\begin{aligned}[t]
&w\in V(p)\\
&siempre\\
&nunca\\
&no\: w \models  \varphi\\
&w \models \varphi \text{ y } w \models \psi\\
&w \models \varphi \text{ ó } w \models \psi\\
&w_1 \models \varphi\\
&\exists_1 \ge 0: w_i \models \varphi \text{ y } \forall0 \le j < i,  w_i \models \varphi\\
\end{aligned}
\end{equation*}}
En donde $w_i$ significa tomar el sufijo de la secuencia que comienza en $i$ (incluido).
$$w = x_0x_1x_2... \Rightarrow w_1 = x_1x_2x_3...$$

\section{Lógica Temporal de Tiempo Lineal con Fluentes}
En esta sección se aborda una extensión a la Lógica Temporal Lineal llamada Fluent Linear Temporal Logic (\emph{FLTL}).
Si bien la lógica \emph{LTL} presentada hasta aquí parece ser muy adecuada para expresar propiedades sobre sistemas de transición de estados, existen \textit{n} circunstancias para las cuales sus descripciones (fórmulas) resultan excesivamente complejas. Los sistemas de transición de estados son esencialmente sistemas orientados a eventos. De este modo surge la pregunta sobre cómo es posible referirse a estados en tales condiciones, o dicho de otro modo, cuáles deben ser las proposiciones atómicas a partir de las cuales construir fórmulas. Una alternativa sería convertir la ocurrencia de cada evento en una proposición que sería verdadera exactamente luego de la ocurrencia de éste, y falsa en otro momento. Esto no supone una solución viable dado que los LTS obtenidos son esencialmente \textit{interleavings}\footnote{Haciendo caso al significado de la palabra ``\textit{interleave}'' (intercalar), un interleaving es una traza que se obtiene intercalando otras trazas que se ejecutan en paralelo. En un sistema concurrente los interleavings son todas las ejecuciones posibles del sistema, producto de intercalar el comportamiento de todos los flujos de control de toda manera posible.} de 2 de procesos, y en consecuencia, sólo una proposición puede ser verdadera en cada momento. De este modo la escritura de propiedades relativamente simples resulta en una tarea dificultosa.
La solución a este problema consiste en la utilización de $fluentes$, que son una manera abstracta de referirse a estados en sistemas basados en eventos. Formalmente, un $fluente$ es
un par de conjuntos de eventos.

$$fl = \langle\{ s_1,..., s_n\}, \{e_1,...,e_m\}\rangle$$

En donde los eventos en el conjunto $\{ s_1,..., s_n\}$ son los eventos que activan el fluente, mientras que los eventos en $\{e_1,...,e_m\}$ son los que deshabilitan el fluente. Dicho de otro modo, el fluente se vuelve verdadero tras la ocurrencia de un evento del conjunto $\{ s_1,..., s_n\}$ y falso tras la ocurrencia de un evento perteneciente a $\{e_1,...,e_m\}$.\\
A continuación se presenta un ejemplo que muestra cómo los fluentes pueden ser utilizados como proposiciones en fórmulas de lógica temporal lineal y cómo éstos permiten referirse a estados en un sistema.\\
\newline
\textbf{Ejemplo}\\
En este ejemplo se podrá visualizar un sistema simple de una luz. La figura 2.2 refleja el funcionamiento de este sistema. Como se puede ver el sistema cuenta de tan solo dos estados que corresponden a si la luz se encuentra \textit{apagada} (estado cero en la figura) o \textit{prendida} (estado uno en la figura). A modo de entender el ejemplo los estados simplemente ocurren y no existen agentes que ejecuten los eventos.\\

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{figura1.eps}
\caption{ Ejemplo de grafo con estados}
\end{figure}


La motivación de este ejemplo es el uso de fluentes como medio para describir estados en sistemas, que como éste, se basan en eventos. Circunscribiendo el ejemplo a una sola luz podríamos proponer los siguientes fluentes:\\

$$\textit{ON}= \la\{\text{on}\},\{\text{off}\}\ra$$
$$\textit{OFF}= \la\{\text{off}\},\{\text{on}\}\ra$$

Lo cual no aporta novedad alguna. Aún más, se podría argüir que, en el caso de ejemplos como éste donde un autómata describe el comportamiento de un proceso (que no es una composición de procesos menores), el uso de fluentes dificulta la tarea. Es más fácil, referirse a los estados directamente por su nombre. Sin embargo el problema surge cuando el sistema de transición de estados es la composición paralela de varios sistemas.

Como se mencionó al principio, el sistema de este ejemplo consta de dos luces que se comportan como lo descripto en la figura 2.1. Un autómata describiendo el comportamiento de las dos luces funcionando en paralelo será como se muestra en la figura 2.2.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{figura2.eps}
\caption{ Grafo describiendo el comportamiento de dos luces en paralelo}
\end{figure}

Teniendo en cuenta el autómata de la figura 2.2, considérese que se desea identificar el hecho de que la luz $l_0$ se encuentre encendida. En el ejemplo de la figura 2.1 esto era muy sencillo pues el diagrama constaba de sólo dos estados: uno encendido y el otro apagado. Más aún, en ese tipo de ejemplos se podría introducir una variable proposicional por cada estado que indicase la estadía en el mismo. Sin embargo en el modelo de la figura 2.2 esto no es tan sencillo. Dado que en este último ejemplo el autómata es una composición paralela de otros dos, los estados de una luz no son identificables como antes, sino que se encuentran dispersos sobre una multiplicidad de estados del sistema general. De hecho, no hay un sólo estado (en el sistema) donde $l_0$ esté encendida; esto sucede ahora en dos estados: 1 y 3. Es aquí donde el uso de fluentes prueba su utilidad. Para capturar los estados de cada una de las luces en el sistema general, basta considerar los fluentes:

$$\textit{ON(i)}= \la\{l_i.\text{on}\},\{l_i.\text{off}\}\ra , i \in [\text{0.,1}]$$
$$\textit{OFF(i)}= \la\{l_i.\text{off}\},\{l_i.\text{on}\}\ra  , i \in [\text{0.,1}]$$

Aquí también se aprecia cómo es posible definir fluentes parametrizados. La expresión \textit{ON(i)} no define un sólo fluente, sino una multiplicidad de ellos. Al fijar el parámetro \textit{i} se tiene como resultado la definición de un fluente, que se obtiene reemplazando el nombre del parámetro por su valor actual en el cuerpo de la definición.\\
Utilizando estos fluentes como proposiciones se pueden escribir propiedades al estilo \emph{LTL}. La lógica resultante de ésto se denomina Fluent Linear Temporal Logic (\emph{FLTL}).

\indent
$$\textit{``En todo momento el sistema puede alcanzar un estado}$$
$$\textit{donde ambas luces estén encendidas''}$$
$$\Box(\textit{ON}(1) \land \textit{ON}(2))$$

Claramente la composición en paralelo de mas cantidad de sub-sistemas, y/o una mayor complejidad de cada uno de estos, hace que el sistema de transición de estados final crezca rápidamente. De modo que el uso de fluentes es una alternativa muy útil a la hora de
caracterizar estados en este tipo de sistemas.


\section{Sistema de transición de estados}
Un sistema de transición de estados es un tipo de máquina abstracta utilizada para el estudio de la computación. Éste consta de un conjunto de estados y transiciones entre ellos. Las transiciones a su vez están etiquetadas con valores (nombres o etiquetas) de un conjunto dado. Las etiquetas pueden aparecer en más de una transición saliente de un mismo estado; de modo que los LTS pueden tener comportamiento no-determinístico. Los LTS son una herramienta útil para el modelado de sistemas o procesos basados en eventos.

\subsubsection{Definición}
Un LTS es una 4-upla de la forma:
$$L = \langle S,A, \Lambda, q_0\rangle$$
en donde:

\begin{itemize}
\item $ S $ es un conjunto finito de estados.
\item $ A $ es el alfabeto del sistema de transición de estados.
\item $ \Lambda \subseteq S $ X $A$ X $S $ es la relación de transición entre los estados del LTS.
\item $ q_0 $ es el estado inicial del LTS.
\end{itemize}

\section{FSP}
\emph{FSP} es un cálculo de procesos tal como los desarrollados por Milner (1989), Calculus of Communicating Systems (CCS), y Hoare (1985), Communicating Sequential Processes (CSP), para una descripción y el razonamiento preciso sobre sistemas concurrentes. La mayor diferencia con estos es que la sintaxis de \emph{FSP} fue diseñada para ser fácilmente analizable. Estas descripciones pueden ser representadas mediante el uso de un LTS.

\subsection{Sintaxis}
Una especificación en \emph{FSP} puede estar compuesta por alguna de las siguientes construcciones sintácticas.

\begin{itemize}
\item \textbf{Procesos:}
Los procesos son el bloque de construcción mas básico del lenguaje. Un proceso está formado por uno o mas procesos locales delimitados por comas. Al final de la definición de un proceso es obligatorio el uso de un punto. Los identificadores de procesos deben comenzar con mayúscula. Existen dos procesos primitivos locales: \textbf{STOP} y \textbf{ERROR}.

\item \textbf{Prefijo de acciones:}
El prefijado de acciones antepone una acción a un proceso. Es decir, si \textbf{a} es el nombre de una acción y \textbf{P} el nombre de un proceso, entonces $a -> P$ es un proceso que sincroniza con el evento \textbf{a} y luego se comporta como \textbf{P}. Los nombres de acciones deben ser identificadores que comiencen con minúscula y pueden contener valores computados a partir de expresiones.

\item \textbf{Elección:}
El operador de elección permite especificar un punto a partir del cual el comportamiento de un proceso varía según la ocurrencia de ciertos eventos. Supongamos que \textbf{x} e \textbf{y} son dos acciones y que \textbf{P} y \textbf{Q} son dos procesos, entonces $(x->P | y->Q)$ es un proceso que sincroniza con \textbf{x} o bien con \textbf{y} y luego, según cual haya sido el caso, se comporta como \textbf{P} o como \textbf{Q} respectivamente.

\item \textbf{Acciones con guarda:}
Dentro de una definición con operador \textit{elección} ($|$) es posible añadir guardas a las alternativas. En una definición del tipo $(\textbf{when B }x -> P | y -> Q)$ ambas guardas son elegibles si \textbf{B} es verdadera, pero la guarda prefijada con \textbf{x} no puede ser elegida en caso de que \textbf{B} sea falsa.

\item \textbf{Extensión de alfabeto:}
El \textit{alfabeto} de un proceso es el conjunto de acciones con las que éste puede sincronizar. El uso de operador \textbf{+} sirve para añadir acciones al alfabeto de un proceso. La construcción \textbf{P + S} expande el alfabeto de \textbf{P} de modo que también contenga las acciones de el conjunto \textbf{S}.

\item \textbf{Composición paralela:}
La composición paralela de dos procesos define un nuevo proceso que contiene todos los \textit{interleavings} posibles de acciones de cada uno de sus constituyentes. Si bien ésta representa la ejecución en paralelo de cada proceso, es fundamental remarcar que, si dos procesos comparten una misma acción, entonces deben ejecutarla de forma simultánea
(necesariamente deben sincronizarse).

\item \textbf{Replicación:}
La replicación es equivalente a múltiples composiciones paralelas. Ésta se simboliza mediante la palabra reservada \textbf{forall}.

\item \textbf{Labeling:}
La operación de \textit{labeling} tiene el efecto de prefijar un identificador a todos los nombres en el alfabeto de un proceso. La expresión \textbf{a:P} prefija todos los nombres del alfabeto de \textbf{P} con \textbf{a}.

\item \textbf{Sharing:}
Esta operación sirve para modelar situaciones en las que existe un recurso compartido. Se denota mediante \textbf{::}. Supongamos que el recurso a compartir está modelado con un cierto proceso \textbf{P}. Entonces la expresión \textbf{${a_1,...,a_n}::P$} reemplaza cada nombre \textbf{m} en el alfabeto de \textbf{P} por los nombres \textbf{$a_1,...,a_n$}. Además, cada transición de la forma \textbf{$(m->Q)$} en la definición de \textbf{P} es reemplazada por \textbf{$(a_1,...,a_n->Q)$}.

\item \textbf{Operadores de prioridad:}
Existen dos operadores que permiten modelar prioridad en \emph{FSP}, estos son: \textbf{$<<$} y \textbf{$>>$}. Cada vez que el sistema se encuentre en un estado en el que puede elegir dos o más acciones, los operadores de prioridad pueden ser utilizados para ponderar la elección de algunas sobre otras.
\end{itemize}

A continuación un ejemplo simple de un modelo del problema conocido como el productor-consumidor utilizando un \textit{buffer}.

\begin{figure}[htp] \centering{
\includegraphics[scale=0.8]{graphs/producerConsumer.pdf}}
\caption{Diseño de FLWAnalizer}
\end{figure}

La especificación de este modelo en \textit{FSP} es la siguiente:

\begin{shaded}
\begin{align*}
PROD &= (produce ->PROD)\\\\
CONS &= (consume ->CONS)\\\\
BUFF&(N=3) = STATE[0]\\
STAT&E[i:0..N] = (\\
&when (i<N) put[i] ->STATE[i+1]\\
&| when (i>0) get[i] ->STATE[i-1])\\\\
\| BOU&NDEDBUFFER = (PROD \| BUFF(Size) \| CONS)\\
&/\{ put[0..Size-1]/produce, get[1..Size]/consume \}
\end{align*}
\end{shaded}

\section{Lenguajes para el Modelado de Procesos de Negocios}
En esta sección analizaremos diferentes lenguajes para el modelado de Procesos de Negocios, el objetivo es mostrar cómo todos los lenguajes de modelado de procesos de negocios comparten un conjunto de primitivas para el modelado de
diferentes tipos de flujo de control.
Por otra parte se presentará a \emph{YAWL} como otro lenguaje para el modelado de \textit{workflow} describiendo sus características principales como los elementos que lo componen.

\subsection{Introducción}
Un Proceso de Negocio puede definirse sucintamente como sigue:
$$\textit{``Es una colección de actividades relacionadas y estructuradas con el fin de producir}$$
$$\textit{un servicio o producto específico.''\cite{Ricci2012}}$$

Dado que el presente trabajo trata con el modelado de los procesos de negocios, enfocaremos nuestra atención en la parte \textit{``...colección de actividades relacionadas y estructuradas...''}. Cualquier metodología o lenguaje que sirva a este fin debe ser capaz de capturar y permitir describir exitosamente cualquier tipo de relación de secuencialidad entre tareas, así como puntos de decisión, bifurcación, unión y sincronización de las actividades. Si bien nuestra propuesta de especificación y análisis de propiedades se focaliza en la utilización de un lenguaje particular, cualquier lenguaje orientado a la especificación del control de flujo podría utilizarse como modelo para la especificación y verificación de propiedades. \\
A continuación se introducirán los Diagramas de Flujo, el lenguaje BPMN y finalmente \emph{YAWL}. Dado que los modelos de \emph{YAWL} se basan el patrones de workflows, introduciremos el concepto y repasaremos aquellos involucrados en este trabajo.

\subsection{Diagramas de Flujo}
Un lenguaje surge quizás como el primero y más utilizado para el modelado de flujos de control: los diagramas de flujo. Sus orígenes se remontan a los años veinte y ha sido ampliamente utilizado en el modelado, tanto de procesos industriales como algoritmos de computadoras.
Un \emph{diagrama de flujo} es un tipo de diagrama que sirve para la representación de procesos o algoritmos, representando de modo gráfico las actividades y el flujo de control entre los mismos. En estos diagramas, los diferentes pasos o actividades se dibujan como rectángulos. El orden en que se deben ejecutar las actividades viene dado por la interconexión de éstas mediante flechas, que representan el flujo de control. El flujo de datos usualmente no está representado en los diagramas de flujo de manera explícita, sino que el mismo pude deducirse de las tareas que representan las actividades del diagrama.\\
A continuación detallamos los objetos que componen este tipo de diagramas y cuya representación gráfica puede observarse en la Figura 2.3.\\\newline

\textbf{Componentes básicos de un diagrama de flujo}

\begin{itemize}
\item \textbf{Símbolo de comienzo y de fin: }Estos símbolos se representan como círculos en el diagrama y suelen llevar las inscripciones \textit{``Start''} y \textit{``End''} dentro de ellos (respectivamente). En algunos casos también se representan como óvalos o rectángulos con puntas redondeadas.
\item \textbf{Flechas: } Describen el \textit{flujo de control.} Una flecha que comienza en un elemento del diagrama y termina en otro especifica el flujo de control desde el componente de partida al de llegada asociados a la misma.
\item \textbf{Actividades o tareas: }Son representados como rectángulos. Describen una actividad simple del proceso, es decir, que no puede descomponerse en sub-actividades.
\item \textbf{Sub-rutinas: }Son representados como rectángulos con líneas verticales dobles. Describen una actividad en el proceso que puede descomponerse. Normalmente su estructura interna se especifica en un diagrama de flujo por separado.
\item \textbf{Actividades de entrada-salida: }Son representados como paralelogramos. Describen la actividad de obtener o enviar datos al exterior. Estos componentes resultan de utilidad durante el modelado de algoritmos.
\item \textbf{Condicional o decisión: }Son representados como rombos y son usados para describir una estructura de control de flujo condicional. Pueden ser considerados como la contraparte diagramática del \textit{if-then-else} de los lenguajes de programación. Estos constan de una flecha de entrada, una condición en base a la cual se bifurca, y de dos flechas de salida, etiquetadas con \textit{``yes''} y \textit{``no''} respectivamente. En algunos casos es posible encontrar múltiples flechas de salida, cada una etiquetada con una condición; ésto no es aconsejable ya que representa una decisión que debería ser descompuesta en otras más simples.
\item \textbf{Intersección: }Generalmente se representan con un punto negro sólido. Describen un punto en donde múltiples flujos de control convergen. Denotan simplemente un punto en la ejecucción del sistema, no deben ser interpretados como un mecanismo de sincronización concurrente. Puede tener varias flechas entrantes pero sólo una saliente.
\item \textbf{Símbolo de concurrencia: }Se representa como una doble línea horizontal. Pueden tener cualquier número de 
flechas entrantes y salientes. Las flechas entrantes deben sincronizar antes de que la ejecución pueda continuar. Luego de ésto todos los flujos salientes son iniciados en paralelo y de modo simultáneo. En el caso donde existe una sola entrada y múltiples salidas el componente se suele denominar \textit{split}; y en el caso de múltiples entradas y sólo una salida se lo suele denominar \textit{join}.
\end{itemize}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{images/diagramaDeFlujo.png}
\caption{Diagrama De Flujo}
\end{figure}

\subsection{BPMN}
BPMN (Business Process Modeling Notation) es un lenguaje estandarizado para el modelado de procesos de negocios\cite{BPMN20}. Es una notación gráfica que permite su especificación mediante la creación de diagramas de flujo de trabajo. BPMN fue desarrollada por la Business Process Management Initiative (BPMI), y es actualmente mantenida por la Object Management Group (OMG). El objetivo primario de BPMN es proveer una notación que sea legible e intuitiva para todos los usuarios, desde analistas que diseñan los procesos de negocios, hasta técnicos responsables de su implementación, incluyendo a las personas responsables de dirigirlos y monitorearlos.\\
El modelado de procesos mediante BPMN se basa en la confección de diagramas. Estos últimos están compuestos por elementos gráficos, cada uno con una representación y significado particular. Su clasificación se detalla a continuación.

\begin{itemize}
\item \textbf{Objetos de Flujo}
\begin{itemize}
\item \textbf{Eventos: } Los eventos modelan algún acontecimiento durante el flujo del proceso. Usualmente tienen una causa o un efecto asociado. El término \textbf{``evento''} es lo suficientemente general para cubrir una amplia gama de fenómenos en un proceso de negocio. El comienzo de una actividad, su finalización, el cambio de estado de un documento, el arribo de un mensaje, pueden todos ser considerados como eventos. Sin embargo BPMN restringe el uso de estos sólo a aquellas situaciones que puedan alterar el flujo de control o el tiempo que las actividades demoran. Los eventos pueden clasificarse en eventos de comienzo, intermedios y fin.
\item \textbf{Actividades:} Las actividades se representan como rectángulos de puntas redondeadas. Una actividades representa un cierto trabajo que es realizado dentro de una organización. Éstas pueden ser simples o compuestas, en el último caso se entiende que pueden ser descompuestas en otras actividades.
\item \textbf{Compuestas (Gateways):} Las compuestas sirven para modelar distintos patrones de flujo de control, divergentes o convergentes, paralelos o no: \textit{branching, merging, joining}. Éstas son representadas mediante rombos que en su interior contienen figuras que especifican el tipo de compuertas existentes así como su reprentación gráfica. En la figura 2.4 se detallan algunas de las compuertas que podrían presentarse en modelos de BPMN.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.6]{images/gatewaysBPMN.png}
\caption{Compuertas PBMN}
\end{figure}

\end{itemize}
\item \textbf{Objetos de Interconexión}
\begin{itemize}
\item \textbf{Flujo secuencial:} El flujo secuencial especifica el orden en el que se deben realizar las actividades dentro de un proceso. Se representan como una flecha sólida con una punta. Ésta denota la dirección del flujo. Adicionalmente los flujos pueden ser \textit{condicionales}, en cuyo caso la flecha se dibuja con un rombo en su inicio, o \textit{flujos por defecto}, que se dibujan con una línea diagonal superpuesta al comienzo de la flecha.
\item \textbf{Flujo de mensajes:} Éste se utiliza para modelar situaciones en la que dos participantes interactuan mediante el envío de mensajes. Un ejemplo de esto en BPMN es cuando dos procesos en diferentes \textit{carriles} intercambian mensajes. Estos últimos se diagraman mediante líneas entrecortadas con un círculo vacío en el comienzo, y una punta vacía al final de la flecha.
\item \textbf{Asociación:} Sirven para asociar datos que no pertenecen al flujo (objetos que representan información, texto, gráficos, etcétera) con elementos del mismo. Se representan mediante líneas punteadas.
\end{itemize}
\item \textbf{Objetos de Agrupamiento}
\begin{itemize}
\item \textbf{Pools:} Los \textit{Pools} se utilizan para especificar un participante en un proceso. Se representan como recuadros que engloban un conjunto de actividades. Establecen una división conceptual entre éstas y las pertenecientes a otros \textit{pools}.
\item \textbf{Lanes:} Se utilizan para subdividir un \textit{pool} y categorizar las actividades dentro de éste con un mayor grado de granularidad.
\end{itemize}
\item \textbf{Artefactos:}
\begin{itemize}
\item \textbf{Objetos de datos:} Los objetos de datos son considerados artefactos ya que no afectan el flujo de control o el flujo de mensajes del proceso de manera directa. Sin embargo éstos brindan información acerca de qué actividades deben ser llevadas a cabo y qué información requieren y/o producen.
\item \textbf{Grupos:} Los grupos son una manera de categorizar las actividades de un diagrama. Éste tipo de agrupamiento no afecta el flujo del diagrama. Estas categorías tiene un fin conceptual y sirven para fines de análisis o documentación.
\item \textbf{Anotaciones:} Son una manera de adjuntar texto en el diagrama. Sirven para proveer información adicional que no puede ser modelada directamente.
\end{itemize}
\end{itemize}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.3]{images/bpmn.png}
\caption{Elementos de modelos BPMN}
\end{figure}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.5]{images/modelBPMN.png}
\caption{Ejemplo de modelo en BPMN}
\end{figure}

\newpage
\subsection{YAWL}
En esta subsección se introduce a \emph{YAWL} (Yet Another Workflow Language) el lenguaje de modelado de procesos de negocios en el que se centra este proyecto. Aquí se introducirán las construcciones y elementos básicas de \emph{YAWL}, como también su semántica, que está basada en Redes de Petri\cite{Petri2003}.

\subsection{¿Qué es YAWL?}
\emph{YAWL} es un lenguaje para el modelado de procesos de negocios. Este lenguaje sustenta su semántica bajo dos grandes pilares, por un lado, un formalismo (Redes de Petri) que dota al lenguaje de ciertos análisis automatizado y por el otro, un conjunto de patrones de workflows que proveen las bases para la construcción de sus modelos.
Este lenguaje es soportado por un potente editor el cual permite modelar los workflows de manera sencilla. Este editor permite manejar tipos complejos e integración con recursos propios de la herramienta y servicios webs entre otras características; y por último cuenta con un motor de ejecución de workflows.\\ En la Figura 2.7 podemos ver un modelo sencillo que caracteriza la realización de la reserva de un viaje, es decir que se puede ademas de realizar el registro del vuelo también realizar lo que podría ser la reserva del hotel si se lo prefiere como el pedido de la renta de un automóvil y luego la realización del pago.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.9]{images/modelExamplYAWL.png}
\caption{Ejemplo de un modelo en \emph{YAWL}}
\end{figure}

Acontinuación se detallaran los componentes del lenguaje y luego se darán a conocer los patrones de workflow mencionados.

\subsection{Componentes del lenguaje}
Cada modelo en este lenguaje es representado por una red principal y las condiciones de inicio y fin. Sin embargo, esta red puede contener otra redes y otras condiciones de inicio y fin. De este modo, un proceso de negocio puede estar representado por varias redes, la principal y las subredes si las tuviera.\\
Dentro de los principales componentes que se encuentran en la realización del modelado podemos mencionar las tareas o actividades que representan la unidad de trabajo de un proceso de negocio, y las \emph{condiciones} que representan estados del workflow, y otros elementos como el INPUT y el OUTPUT que determinan el inicio o fin de workflow respectivamente. Ademas de las tareas simples podemos definir tareas compuestas y múltiples y a cada una de éstas les podemos incluir compuertas que determinaran restricciones en el modelo, además de las regiones de cancelación las cuales veremos mas adelante.\\\newline


\subsubsection{Condiciones}
Las condiciones en los modelos \emph{YAWL} determinan el estado del sistema en general, es decir que actividades ejecuto y que actividades le resta por ejecutar hasta finalizar el flujo. Existen tres tipos de condiciones en estos modelos como se puede identificar en la figura 2.8, las condiciones de entrada, las condiciones de salida o fin y por último las condiciones que se encuentra durante el flujo del modelo. Estas condiciones se detallarán a continuación.

\begin{itemize}
\item \textbf{Condition:} Este componente de modelado representa en que se encuentra el sistema, es decir un workflow llega a este elemento habiendo ejecutado ya una algunas actividades y otras que están por ejecutarse. 
\item \textbf{Input Condition:} O condición de entrada. Este elemento determina el estado inicial del modelo \emph{YAWL}, es decir es el estado en el cual no se ha ejecutado ninguna de las tareas y se encuentra antes de cualquier actividad.
\item \textbf{Outnput Condition:} O condición de salida. Es el elemento que representa que el workflow ya ejecuto algunas actividades y que no quedan actividades por ejecutar. Representa el estado final de la ejecución.
\end{itemize}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.4]{images/yawlConditions.png}
\caption{\textit{Tpo de condiciones en \emph{YAWL}}}
\end{figure}
   
\subsubsection{Actividades o Teras}
Estas actividades que están presentes en los modelos \emph{YAWL}, describen en éstos que tarea o evento se esta ejecutando, es decir que representan los pasos que tiene que realizar un determinado workflow. En la figura 2.9 podemos ver también tres tipos de Tareas, las tareas simples, las tareas compuestas,  las tareas múltiples y un cuarto tipo de tarea que resulta de la combinación de las anteriores. A continuación se detalla cada una de ellas.

\begin{itemize}
\item \textbf{Simple Task:} Determina la actividad basica a ejecutarse dentro de la red. En este tipo de tareas no se puede dividir en sub-actividades.
\item \textbf{Composite Task:} Son otro de los tipos de actividades que utiliza \emph{YAWL} en el modelado y se utilizan para la composición vertical. A cada tarea compuesta le corresponde una única red \emph{YAWL}.
\item \textbf{Multiple Task:} Este tipo de tarea tiene la propiedad de definir un número de instancias de la actividad que representa, con una cota inferior y una superior de instancias que pueden ejecutarse. Estos limites pueden ser estáticos o dinámicos, es decir número fijo de instancias o bien este número puede crecer durante la ejecución. Además también presenta la propiedad de restringir el número de instancias que se deben cumplir para continuar con el flujo de ejecución.
\end{itemize}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.4]{images/yawlTasks.png}
\caption{\textit{Tipo de tareas en \emph{YAWL}}}
\end{figure}
   
 
\subsubsection{Gates} Cada actividad, además de su tarea específica, puede interferir en el control de flujo mediante la especificación de compuertas que se asocian a la misma. Una compuerta para los flujos de entrada (por ejemplo para la sincronización del flujo de control) y otra para el control de salida (distribución del flujo de control). Éstas se pueden ver en la figura 2.10. Los diferentes tipos de compuertas que utiliza \emph{YAWL} para el control de flujo son los siguientes.

\begin{itemize}
\item\textbf{AND-Join} Sólo se iniciará la ejecución de la tarea que tenga este tipo de compuerta siempre que se hayan completado todos los flujos entrantes\\
\item\textbf{AND-Split} Luego de la finalización de la tarea asociada a esta compuerta, el flujo de control se divide en todas las salidas de la tarea, su comportamiento es similar al comando fork.\\
\item\textbf{OR-Join} Este tipo de compuerta generalmente presenta diferentes semánticas que varían según el significado de esperar las tareas activas que precedan una compuerta OR. La semántica que utilizaremos para nuestro análisis asume que la compuerta puede transferir el control cuando al menos una de sus entradas está habilitada.\\
\item\textbf{OR-Split} Luego de la finalización de la tarea asociada a ésta, el control pasa uno o más de los 
flujos salientes de la tarea. La elección del flujo está dada por las guardas de cada salida. En caso de que ninguna guarda se cumpla se activa un flujo saliente que se toma como predeterminada (\textit{default}).\\
\item\textbf{XOR-Join} La tarea asociada con ésta se inicia luego de que un flujo entrante se haya completado.\\
\item\textbf{XOR-Split} Luego de la finalización de la tarea asociada a ésta, el control pasa exactamente a uno de los flujos salientes de la tarea. La elección del flujo está dada por las guardas de cada salida. En caso de que ninguna guarda se cumpla se activa un flujo saliente que se toma como \textit{default}.\\
\end{itemize}

\begin{figure}[h!]
\centering
\includegraphics[scale=0.4]{images/yawlGates.png}
\caption{\textit{Tipo de compuertas en \emph{YAWL}}}
\end{figure}

\subsubsection{Regiones de cancelación}
En \emph{YAWL}, cada tarea puede tener asociado un conjunto de tareas y condiciones denominado región de cancelación. La interpretación de estas regiones es que, tras la finalización de la tarea, todas las tareas y condiciones dentro de la región son abortadas. Un ejemplo del uso de este elemento puede verse en la Figura 4.3 del Capítulo 4. 

   
\subsection{Patrones de Workflow}
Los patrones de workflow tienen como propósito brindar un concepto básico fundacional para los Procesos de Negocio. Su estudio ofrece un examen exhaustivo de las diversas perspectivas (control de flujo, datos, recursos y manejo de excepciones) que son recurrentes en las descripciones de workflows y cuya semántica debería estar presente en un lenguaje de modelado para tal fin. Los resultados se pueden utilizar para examinar la conveniencia de un determinado proceso o sistema de lenguaje de flujo de trabajo para un proyecto en particular, la evaluación de sus puntos fuertes y debilidades relativas de los distintos enfoques para especificar procesos, implementación de ciertos requisitos de negocio en un determinado sistema de información, y como base para el desarrollo del lenguaje y de nuevas herramientas.\\\newline
Estos patrones son una recopilación de las características y escenarios más comunes en el modelado de procesos de negocios. Presentan una forma abstracta y genérica de modelar situaciones, ya que no están comprometidos a un lenguaje o tecnología en particular. Al mismo tiempo proporcionan una base conceptual para los lenguajes de modelado de workflows, que si bien aparentan compartir una misma base conceptual y un conjunto de construcciones comunes, difieren en gran medida en cuanto a su capacidad expresiva.\\\newline
Podemos separar los patrones de workflow en cuatro grandes categorías: \textit{patrones de control de flujo}, \textit{patrones de control de datos}, \textit{patrones de control de recursos} y \textit{patrones para el manejo de excepciones}.\\\newline
A continuación se detallará algunos de los patrones de control de flujo mas importantes tomados de \cite{Ricci2012} para la realización del presente trabajo\footnote{En caso de que se desee ver el resto de los patrones en \cite{WorkflowPattern} donde se encontrará mayor detalle de todos ellos no obstante en este trabajo solo serán detallados algunos de los patrones de control de flujo}.\\\newline


\begin{table}[htp]
        \centering
	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{5}{1.5cm}{\centering Patrón 1} 	&   \textbf{Nombre}  &  Secuence	\\
		\cline{2-3}
			& \multirow{3}{3cm}{\centering\textbf{Descripción}}	&	Composición secuencial de tareas. Una actividad se ejecuta luego de que otra termina con su ejecución.	\\
		\cline{2-3}
			&	\multirow{2}{3cm}{\centering\textbf{Ejemplo}}	&	Un ticket es impreso luego de que se ha realizado el pago por la compra.	\\
		\hline
	\end{tabular}



	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{11}{1.5cm}{\centering Patrón 2} 	&   \textbf{Nombre}  &  Parallel Split	\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la divergencia de un flujo de control en dos o más. Todos estos son ejecutados concurrentemente y se inician de manera simultánea. También se lo suele denominar \textit{parallel routing}, \textit{fork} o \textit{AND-Split}.\\
		\cline{2-3}
			&	\multirow{4}{3cm}{\centering\textbf{Ejemplo}}	&	Cuando se realiza una compra, la emisión de una factura y el empaquetado del producto son iniciadas en paralelo.\\
		\hline
	\end{tabular}


	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{13}{1.5cm}{\centering Patrón 3} 	&   \textbf{Nombre}  &  Synchronization\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la convergencia de múltiples flujos de control. Cuando todos los flujos de control entrantes han arribado, el control se pasa el flujo saliente. También se lo suele denominar \textit{rendezvous}, \textit{sychronizer} o \textit{AND-Join}.\\
		\cline{2-3}
			&	\multirow{6}{3cm}{\centering\textbf{Ejemplo}}	&	Al realizar un retiro dinero en un cajero automático,
éste sólo puede volver a la pantalla inicial luego de que las actividades de emisión de ticket y entrega del dinero hayan finalizado.\\
		\hline
	\end{tabular}
\end{table}

\begin{table}[htp]
        \centering
	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{23}{1.5cm}{\centering Patrón 4} 	&   \textbf{Nombre}  &  Exclusive Choice\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa un punto de elección en el flujo de control. Cuando el flujo entrante arriba, el control pasa a exactamente uno de los flujos salientes basándose en una condición lógica asociada al punto de elección. También se lo suele denominar \textit{XOR-Split}, \textit{exclusive OR-Split} o \textit{switch}.\\
		\cline{2-3}
			&	\multirow{15}{3cm}{\centering\textbf{Ejemplo}}	&	\begin{itemize}\item En una elección, luego de la actividad de conteo de votos, se puede comenzar con la actividad de anuncio de resultados o con la de recuento de votos, dependiendo
de los resultados del primer conteo.
\item Un grupo de alumnos planifica la asistencia a un congreso, dependiendo de la cantidad de personas se debe comenzar la actividad de reservar un automóvil, una traffic, o un colectivo.
 \end{itemize}\\
		\hline
	\end{tabular}

	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{10}{1.5cm}{\centering Patrón 5} 	&   \textbf{Nombre}  & Simple Merge\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la convergencia de múltiples flujos de control en uno solo. Cuando algún flujo entrante arriba el control se pasa el flujo saliente. También se lo suele denominar \textit{XOR-Join},\textit{exclusive OR-Join}, \textit{synchronous join} o \textit{merge}.\\
		\cline{2-3}
			&	\multirow{4}{3cm}{\centering\textbf{Ejemplo}}	&	Luego de la realización de la actividad de pago con tarjeta de crédito o la de pago en efectivo, el proceso continua con la realización de la actividad de emisión de factura.\\
		\hline
	\end{tabular}
\end{table}


\begin{table}[htp]
        \centering
	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{10}{1.5cm}{\centering Patrón 6} 	&   \textbf{Nombre}  & Multi-Choise\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la división de un flujo en dos o más flujos. Todos los flujos salientes se activan concurrentemente y en simultáneo. Cualquier cantidad de flujos salientes pueden ser activados, no es necesario que sea sólo uno, ni que sean todos ellos. También es llamado \textit{Conditional Routing}, \textit{selection}, \textit{OR-Split} o \textit{multiple choice}.\\
		\cline{2-3}
			&	\multirow{4}{3cm}{\centering\textbf{Ejemplo}}	&	Cuando una llamada de emergencia es atendida,
dependiendo de la naturaleza de la misma, se pueden iniciar las actividades de envío de la policía, del servicio médico y de los bomberos. Cualquier combinación de estas actividades puede ser disparada.\\
		\hline
	\end{tabular}


	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{10}{1.5cm}{\centering Patrón 7} 	&   \textbf{Nombre}  & Structured Synchronizing Merge\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la sincronización de múltiples flujos de control, luego de que todos los flujos entrantes han llegado al punto de sincronización el control pasa al flujo saliente. Se diferencia de la sincronización usual en que no se espera que todos los flujos entrantes arriben, sino sólo aquellos activos. Este patrón es la contraparte al patrón anterior. También se lo denomina \textit{Synchronizing Join}, \textit{synchronizer} o \textit{OR-Join}.\\
		\cline{2-3}
			&	\multirow{4}{3cm}{\centering\textbf{Ejemplo}}	&	Cuando una llamada de emergencia es atendida,
dependiendo de la naturaleza de la misma, se pueden iniciar las actividades de envío de la policía, del servicio médico y de los bomberos. Cuando todos los vehículos de emergencia arriban, se comienza con el traslado del paciente.\\
		\hline
	\end{tabular}
\end{table}
\newpage
Estos patrones extraídos de\cite{Ricci2012} son algunos de todos los patrones que podemos encontrar en \cite{WorkflowPatterns2003} y \cite{WorkflowPatterns2006}  .Sin embargo, como se puede apreciar, los patrones de workflow se encargan de capturar conceptos básicos del modelado de procesos, escenarios que se repiten constantemente y construcciones que siempre están presentes --sea de modo directo o indirecto-- en cualquier lenguaje que se trate.\\\newline